1 /-
2 Copyright (c) 2019 Zhouhang Zhou. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Zhouhang Zhou
5 -/
6
7 import algebra.ordered_field
src └───────────────────┘
8 import tactic.linarith tactic.ring
src └─────────────┘ └─────────┘
9
10 /-!
11 # Quadratic discriminants and roots of a quadratic
12
13 This file defines the discriminant of a quadratic and gives the solution to a quadratic equation.
14
15 ## Main definition
16
17 The discriminant of a quadratic `a*x*x + b*x + c` is `b*b - 4*a*c`.
18
19 ## Main statements
20 • Roots of a quadratic can be written as `(-b + s) / (2 * a)` or `(-b - s) / (2 * a)`,
21 where `s` is the square root of the discriminant.
22 • If the discriminant has no square root, then the corresponding quadratic has no root.
23 • If a quadratic is always non-negative, then its discriminant is non-positive.
24
25 ## Tags
26
27 polynomial, quadratic, discriminant, root
28 -/
29
30 variables {α : Type*}
31
32 section lemmas
33
34 variables [linear_ordered_field α] {a b c : α}
id └──────────────────┘
src └──────────────────┘
typ └──────────────────┘
35
36 lemma exists_le_mul_self : ∀ a : α, ∃ x : α, a ≤ x * x :=
id ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴
37 begin
st └─────
38 assume a, cases le_total 1 a with ha ha,
id └──────┘ ┴
src └──────┘ └────┘└──────┘└─┘ └─────────┘
typ └──────┘ └────┘└──────┘└─┘┴└─────────┘
doc └──────┘ └────┘ └─┘ └─────────┘
txt └──────┘ └────┘ └─┘ └─────────┘
par └──────┘ └────┘ └─┘ └─────────┘
pid └──────┘ ┴ └─┘ └─────────┘
st ─────────┘└─────────────────────────────┘└─
39 { use a, exact le_mul_of_ge_one_left (by linarith) ha },
id ┴ └───────────────────┘ └┘
src └──┘ └────┘└───────────────────┘┴ ┴└──────┘└┘ ┴
typ └──┘┴ └────┘└───────────────────┘┴ ┴└──────┘└┘└┘┴
doc └──┘ └────┘ ┴ ┴└──────┘└┘ ┴
txt └──┘ └────┘ ┴ ┴└──────┘└┘ ┴
par └──┘ └────┘ ┴ ┴└──────┘└┘ ┴
pid ┴ ┴ ┴ └─────────┘ ┴
st ───┘└───┘└───────────────────────────────┘└───────┘└───┘└┘└
40 { use 1, linarith }
src └───┘ └───────┘
typ └───┘ └───────┘
doc └───┘ └───────┘
txt └───┘ └───────┘
par └───┘ └───────┘
pid ┴┴ ┴
st ────────┘└─────────┘└─
41 end
st ──┘
42
43 lemma exists_lt_mul_self : ∀ a : α, ∃ x : α, a < x * x :=
id ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴
44 begin
st └─────
45 assume a, rcases (exists_le_mul_self a) with ⟨x, hx⟩,
id └────────────────┘ ┴
src └──────┘ └─────┘ └────────────────┘┴ └────────────┘
typ └──────┘ └─────┘ └────────────────┘┴┴└────────────┘
doc └──────┘ └─────┘ ┴ └────────────┘
txt └──────┘ └─────┘ ┴ └────────────┘
par └──────┘ └─────┘ ┴ └────────────┘
pid └──────┘ ┴ ┴ └────────────┘
st ─────────┘└──────────────────────────────────────────┘└─
46 cases le_total 0 x with hx' hx',
id └──────┘ ┴
src └────┘└──────┘└─┘ └───────────┘
typ └────┘└──────┘└─┘┴└───────────┘
doc └────┘ └─┘ └───────────┘
txt └────┘ └─┘ └───────────┘
par └────┘ └─┘ └───────────┘
pid ┴ └─┘ └───────────┘
st ────────────────────────────────┘└─
47 { use (x + 1),
id ┴ ┴
src └──┘ ┴┴└─┘
typ └──┘ ┴┴┴└─┘
doc └──┘ ┴ └─┘
txt └──┘ ┴ └─┘
par └──┘ ┴ └─┘
pid ┴ ┴ └─┘
st ───┘└─────────┘└─
48 have : (x+1)*(x+1) = x*x + 2*x + 1, ring,
id ┴ ┴ ┴
src └─────┘ └┘┴ └─┘┴┴ ┴ └┘ ┴ └┘ └──┘
typ └─────┘ └┘┴ └─┘┴┴ ┴ └┘ ┴┴ └┘ └──┘
doc └─────┘ └┘ └─┘ ┴ ┴ └┘ ┴ └┘ └──┘
txt └─────┘ └┘ └─┘ ┴ ┴ └┘ ┴ └┘ └──┘
par └─────┘ └┘ └─┘ ┴ ┴ └┘ ┴ └┘ └──┘
pid └───┘└┘ └┘ └─┘ ┴ ┴ └┘ ┴ ┴┴
st ─────────────────────────────────────┘└────┘└─
49 exact lt_of_le_of_lt hx (by rw this; linarith) },
id └────────────┘ └┘ └──┘
src └────┘└────────────┘┴ ┴ ┴└─┘ └┘└──────┘└┘
typ └────┘└────────────┘┴└┘┴ ┴└─┘└──┘└┘└──────┘└┘
doc └────┘ ┴ ┴ ┴└─┘ └┘└──────┘└┘
txt └────┘ ┴ ┴ ┴└─┘ └┘└──────┘└┘
par └────┘ ┴ ┴ ┴└─┘ └┘└──────┘└┘
pid ┴ ┴ ┴ └──┘ └─────────┘┴
st ──────────────────────────────┘└────────────────┘└┘└┘└
50 { use (x - 1),
id ┴ ┴
src └──┘ ┴┴└─┘
typ └──┘ ┴┴┴└─┘
doc └──┘ ┴ └─┘
txt └──┘ ┴ └─┘
par └──┘ ┴ └─┘
pid ┴ ┴ └─┘
st ──────────────┘└─
51 have : (x-1)*(x-1) = x*x - 2*x + 1, ring,
id ┴
src └─────┘ └┘ └─┘ ┴ ┴ └┘ ┴ └┘ └──┘
typ └─────┘ └┘ └─┘ ┴ ┴ └┘ ┴┴ └┘ └──┘
doc └─────┘ └┘ └─┘ ┴ ┴ └┘ ┴ └┘ └──┘
txt └─────┘ └┘ └─┘ ┴ ┴ └┘ ┴ └┘ └──┘
par └─────┘ └┘ └─┘ ┴ ┴ └┘ ┴ └┘ └──┘
pid └───┘└┘ └┘ └─┘ ┴ ┴ └┘ ┴ ┴┴
st ─────────────────────────────────────┘└────┘└─
52 exact lt_of_le_of_lt hx (by rw this; linarith) }
id └────────────┘ └┘ └──┘
src └────┘└────────────┘┴ ┴ ┴└─┘ └┘└──────┘└┘
typ └────┘└────────────┘┴└┘┴ ┴└─┘└──┘└┘└──────┘└┘
doc └────┘ ┴ ┴ ┴└─┘ └┘└──────┘└┘
txt └────┘ ┴ ┴ ┴└─┘ └┘└──────┘└┘
par └────┘ ┴ ┴ ┴└─┘ └┘└──────┘└┘
pid ┴ ┴ ┴ └──┘ └─────────┘┴
st ──────────────────────────────┘└────────────────┘└┘└─
53 end
st ──┘
54
55 end lemmas
56
57 variables [linear_ordered_field α] {a b c x : α}
id └──────────────────┘
src └──────────────────┘
typ └──────────────────┘
58
59 /-- Discriminant of a quadratic -/
60 def discrim [ring α] (a b c : α) : α := b^2 - 4 * a * c
id └──┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴
src └──┘ ┴ ┴ ┴ ┴
typ └──┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴
61
62 /--
63 A quadratic has roots if and only if its discriminant equals some square.
64 -/
65 lemma quadratic_eq_zero_iff_discrim_eq_square (ha : a ≠ 0) :
id ┴ ┴
src ┴
typ ┴ ┴
66 ∀ x : α, a * x * x + b * x + c = 0 ↔ discrim a b c = (2 * a * x + b)^2 :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────┘
67 assume x, iff.intro
id ┴ └───────┘
src └───────┘
typ ┴ └───────┘
68 (assume h, calc
id ┴
typ ┴
69 discrim a b c = 4*a*(a*x*x + b*x + c) + b*b - 4*a*c : by rw [h, discrim]; ring
id └─────┘ ┴ ┴ ┴ ┴┴┴ ┴┴┴┴┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴┴┴┴ ┴ └─────┘
src └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └┘└─────┘┴ └────
typ └─────┘ ┴ ┴ ┴ ┴┴┴ ┴┴┴┴┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴┴┴┴ └──┘┴└┘└─────┘┴ └────
doc └─────┘ └──┘ └┘└─────┘┴ └────
txt └──┘ └┘ ┴ └────
par └──┘ └┘ ┴ └────
pid └┘ └┘ ┴ └
st └────┘└───────┘┴└──────
70 ... = (2*a*x + b)^2 : by ring)
id ┴┴┴┴ ┴ ┴ ┴
src ─────┘ ┴ ┴ ┴ ┴ └──┘
typ ─────┘ ┴┴┴┴ ┴ ┴ ┴ └──┘
doc ─────┘ └──┘
txt ─────┘ └──┘
par ─────┘ └──┘
pid ─────┘
st ─────┘ └───┘
71 (assume h,
id ┴
typ ┴
72 have ha : 2*2*a ≠ 0 := mul_ne_zero (mul_ne_zero two_ne_zero two_ne_zero) ha,
id ┴ ┴┴ ┴ └─────────┘ └─────────┘ └─────────┘ └─────────┘ └┘
src ┴ ┴ ┴ └─────────┘ └─────────┘ └─────────┘ └─────────┘
typ ┴ ┴┴ ┴ └─────────┘ └─────────┘ └─────────┘ └─────────┘ └┘
73 eq_of_mul_eq_mul_left_of_ne_zero ha $
id └──────────────────────────────┘ └┘
src └──────────────────────────────┘
typ └──────────────────────────────┘ └┘
doc └──────────────────────────────┘
74 calc
75 2 * 2 * a * (a * x * x + b * x + c) = (2*a*x + b)^2 - (b^2 - 4*a*c) : by ring
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴┴┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴┴┴ └────
doc └────
txt └────
par └────
pid └
st └─────
76 ... = 0 : by { rw [← h, discrim], ring }
id ┴ └─────┘
src ─────┘ └────┘ └┘└─────┘┴ └───┘
typ ─────┘ └────┘┴└┘└─────┘┴ └───┘
doc ─────┘ └────┘ └┘└─────┘┴ └───┘
txt ─────┘ └────┘ └┘ ┴ └───┘
par ─────┘ └────┘ └┘ ┴ └───┘
pid ─────┘ └──┘ └┘ ┴ ┴
st ─────┘ └────────┘└───────┘└──────┘└┘
77 ... = 2*2*a*0 : by ring)
id ┴ ┴┴┴
src ┴ ┴ ┴ └──┘
typ ┴ ┴┴┴ └──┘
doc └──┘
txt └──┘
par └──┘
st └───┘
78
79 /-- Roots of a quadratic -/
80 lemma quadratic_eq_zero_iff (ha : a ≠ 0) {s : α} (h : discrim a b c = s * s) :
id ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └─────┘ ┴ ┴
typ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────┘
81 ∀ x : α, a * x * x + b * x + c = 0 ↔ x = (-b + s) / (2 * a) ∨ x = (-b - s) / (2 * a) := assume x,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
82 begin
st └─────
83 rw [quadratic_eq_zero_iff_discrim_eq_square ha, h, pow_two, mul_self_eq_mul_self_iff],
id └─────────────────────────────────────┘ └┘ ┴ └─────┘ └──────────────────────┘
src └──┘└─────────────────────────────────────┘┴ └┘ └┘└─────┘└┘└──────────────────────┘┴
typ └──┘└─────────────────────────────────────┘┴└┘└┘┴└┘└─────┘└┘└──────────────────────┘┴
doc └──┘└─────────────────────────────────────┘┴ └┘ └┘ └┘ ┴
txt └──┘ ┴ └┘ └┘ └┘ ┴
par └──┘ ┴ └┘ └┘ └┘ ┴
pid └┘ ┴ └┘ └┘ └┘ ┴
st ───────────────────────────────────────────────┘└─┘└───────┘└────────────────────────┘└──
84 have ne : 2 * a ≠ 0 := mul_ne_zero two_ne_zero ha,
id ┴ ┴ ┴ └─────────┘ └─────────┘ └┘
src └──────────┘┴┴ ┴┴└────┘└─────────┘┴└─────────┘┴
typ └──────────┘┴┴┴┴┴└────┘└─────────┘┴└─────────┘┴└┘
doc └──────────┘ ┴ ┴ └────┘ ┴ ┴
txt └──────────┘ ┴ ┴ └────┘ ┴ ┴
par └──────────┘ ┴ ┴ └────┘ ┴ ┴
pid └─────┘└───┘ ┴ ┴ ┴└───┘ ┴ ┴
st ──────────────────────────────────────────────────┘└─
85 have : x = 2 * a * x / (2 * a) := (mul_div_cancel_left x ne).symm,
id ┴ ┴ ┴ ┴ └─────────────────┘ ┴ └┘
src └─────┘ ┴┴└─┘ ┴ ┴ ┴ ┴┴┴ └┘ ┴ └───┘ └─────────────────┘┴ ┴└┘└────┘
typ └─────┘ ┴┴└─┘ ┴ ┴ ┴┴┴┴┴ └┘ ┴┴└───┘ └─────────────────┘┴┴┴└┘└────┘
doc └─────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └───┘ ┴ ┴ └────┘
txt └─────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └───┘ ┴ ┴ └────┘
par └─────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └───┘ ┴ ┴ └────┘
pid └───┘└┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴└──┘ ┴ ┴ └───┘┴
st ──────────────────────────────────────────────────────────────────┘└─
86 have h₁ : 2 * a * ((-b + s) / (2 * a)) = -b + s := mul_div_cancel' _ ne,
id ┴ ┴ ┴ ┴ ┴ └─────────────┘ └┘
src └──────────┘ ┴ ┴ ┴ ┴ ┴┴┴ └┘ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ └──┘└─────────────┘└─┘└┘
typ └──────────┘ ┴ ┴ ┴ ┴ ┴┴┴ └┘ ┴ └┘ ┴┴└─┘ ┴ ┴┴ ┴┴└──┘└─────────────┘└─┘└┘
doc └──────────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ └──┘ └─┘
txt └──────────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ └──┘ └─┘
par └──────────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ └──┘ └─┘
pid └─────┘└───┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ └──┘ └─┘
st ────────────────────────────────────────────────────────────────────────┘└─
87 have h₂ : 2 * a * ((-b - s) / (2 * a)) = -b - s := mul_div_cancel' _ ne,
id ┴ ┴ ┴ ┴ └─────────────┘ └┘
src └──────────┘ ┴ ┴ ┴ ┴┴┴ └┘ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ └──┘└─────────────┘└─┘└┘
typ └──────────┘ ┴ ┴ ┴ ┴┴┴ └┘ ┴ └┘ ┴┴└─┘ ┴ ┴┴ ┴┴└──┘└─────────────┘└─┘└┘
doc └──────────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ └──┘ └─┘
txt └──────────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ └──┘ └─┘
par └──────────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ └──┘ └─┘
pid └─────┘└───┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ └──┘ └─┘
st ────────────────────────────────────────────────────────────────────────┘└─
88 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────┘└─
89 { intro h', rcases h', { left, rw h', simpa }, { right, rw h', simpa } },
id └┘ └┘ └┘
src └──────┘ └─────┘ └──┘ └─┘ └────┘ └───┘ └─┘ └────┘
typ └──────┘ └─────┘└┘ └──┘ └─┘└┘ └────┘ └───┘ └─┘└┘ └────┘
doc └──────┘ └─────┘ └──┘ └─┘ └────┘ └───┘ └─┘ └────┘
txt └──────┘ └─────┘ └──┘ └─┘ └────┘ └───┘ └─┘ └────┘
par └──────┘ └─────┘ └──┘ └─┘ └────┘ └───┘ └─┘ └────┘
pid └─┘ ┴ ┴ ┴ ┴ ┴
st ───┘└──────┘└─────────┘└──┘└──┘└─────┘└──────┘└┘└──────┘└─────┘└──────┘└──┘└
90 { intro h', rcases h', { left, rw [h', h₁], ring }, { right, rw [h', h₂], ring } }
id └┘ └┘ └┘ └┘ └┘
src └──────┘ └─────┘ └──┘ └──┘ └┘ ┴ └───┘ └───┘ └──┘ └┘ ┴ └───┘
typ └──────┘ └─────┘└┘ └──┘ └──┘└┘└┘└┘┴ └───┘ └───┘ └──┘└┘└┘└┘┴ └───┘
doc └──────┘ └─────┘ └──┘ └──┘ └┘ ┴ └───┘ └───┘ └──┘ └┘ ┴ └───┘
txt └──────┘ └─────┘ └──┘ └──┘ └┘ ┴ └───┘ └───┘ └──┘ └┘ ┴ └───┘
par └──────┘ └─────┘ └──┘ └──┘ └┘ ┴ └───┘ └───┘ └──┘ └┘ ┴ └───┘
pid └─┘ ┴ └┘ └┘ ┴ ┴ └┘ └┘ ┴ ┴
st ───────────┘└─────────┘└──┘└──┘└──────┘└──┘└──────┘└┘└──────┘└──────┘└──┘└──────┘└───
91 end
st ──┘
92
93 /-- A quadratic has roots if its discriminant has square roots -/
94 lemma exist_quadratic_eq_zero (ha : a ≠ 0) (h : ∃ s, discrim a b c = s * s) :
id ┴ ┴ ┴ ┴┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ └─────┘ ┴ ┴
typ ┴ ┴ ┴ ┴┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────┘
95 ∃ x, a * x * x + b * x + c = 0 :=
id ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
96 begin
st └─────
97 rcases h with ⟨s, hs⟩,
id ┴
src └─────┘ └───────────┘
typ └─────┘┴└───────────┘
doc └─────┘ └───────────┘
txt └─────┘ └───────────┘
par └─────┘ └───────────┘
pid ┴ └───────────┘
st ──────────────────────┘└─
98 use (-b + s) / (2 * a),
id ┴┴ ┴ ┴ ┴ ┴ ┴
src └──┘ ┴ ┴┴┴ └┘┴┴ └┘┴┴ ┴
typ └──┘ ┴┴┴┴┴┴└┘┴┴ └┘┴┴┴┴
doc └──┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴
txt └──┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴
par └──┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴
pid ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴
st ───────────────────────┘└─
99 rw quadratic_eq_zero_iff ha hs,
id └───────────────────┘ └┘ └┘
src └─┘└───────────────────┘┴ ┴
typ └─┘└───────────────────┘┴└┘┴└┘
doc └─┘└───────────────────┘┴ ┴
txt └─┘ ┴ ┴
par └─┘ ┴ ┴
pid ┴ ┴ ┴
st ───────────────────────────────┘└─
100 simp
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ──────┘
101 end
st └─┘
102
103 /-- Root of a quadratic when its discriminant equals zero -/
104 lemma quadratic_eq_zero_iff_of_discrim_eq_zero (ha : a ≠ 0) (h : discrim a b c = 0) :
id ┴ ┴ └─────┘ ┴ ┴ ┴ ┴
src ┴ └─────┘ ┴
typ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴
doc └─────┘
105 ∀ x : α, a * x * x + b * x + c = 0 ↔ x = -b / (2 * a) := assume x,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
106 begin
st └─────
107 have : discrim a b c = 0 * 0 := eq.trans h (by ring),
id └─────┘ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴
src └─────┘└─────┘┴ ┴ ┴ ┴┴└─┘┴└────┘└──────┘┴ ┴ ┴└──┘┴
typ └─────┘└─────┘┴┴┴┴┴┴┴┴└─┘┴└────┘└──────┘┴┴┴ ┴└──┘┴
doc └─────┘└─────┘┴ ┴ ┴ ┴ └─┘ └────┘ ┴ ┴ ┴└──┘┴
txt └─────┘ ┴ ┴ ┴ ┴ └─┘ └────┘ ┴ ┴ ┴└──┘┴
par └─────┘ ┴ ┴ ┴ ┴ └─┘ └────┘ ┴ ┴ ┴└──┘┴
pid └───┘└┘ ┴ ┴ ┴ ┴ └─┘ ┴└───┘ ┴ ┴ └────┘
st ───────────────────────────────────────────────┘└───┘┴└─
108 rw quadratic_eq_zero_iff ha this,
id └───────────────────┘ └┘ └──┘
src └─┘└───────────────────┘┴ ┴
typ └─┘└───────────────────┘┴└┘┴└──┘
doc └─┘└───────────────────┘┴ ┴
txt └─┘ ┴ ┴
par └─┘ ┴ ┴
pid ┴ ┴ ┴
st ─────────────────────────────────┘└─
109 simp
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ──────┘
110 end
st └─┘
111
112 /-- A quadratic has no root if its discriminant has no square root. -/
113 lemma quadratic_ne_zero_of_discrim_ne_square (ha : a ≠ 0) (h : ∀ s : α, discrim a b c ≠ s * s) :
id ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └─────┘ ┴ ┴
typ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────┘
114 ∀ (x : α), a * x * x + b * x + c ≠ 0 :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
115 begin
st └─────
116 assume x h',
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ────────────┘└─
117 rw [quadratic_eq_zero_iff_discrim_eq_square ha, pow_two] at h',
id └─────────────────────────────────────┘ └┘ └─────┘
src └──┘└─────────────────────────────────────┘┴ └┘└─────┘└─────┘
typ └──┘└─────────────────────────────────────┘┴└┘└┘└─────┘└─────┘
doc └──┘└─────────────────────────────────────┘┴ └┘ └─────┘
txt └──┘ ┴ └┘ └─────┘
par └──┘ ┴ └┘ └─────┘
pid └┘ ┴ └┘ ┴└────┘
st ───────────────────────────────────────────────┘└───────┘┴└────┘└─
118 have := h _,
id ┴
src └──────┘ └┘
typ └──────┘┴└┘
doc └──────┘ └┘
txt └──────┘ └┘
par └──────┘ └┘
pid └───┘└─┘ └┘
st ────────────┘└─
119 contradiction
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid ┴
st ───────────────┘
120 end
st └─┘
121
122 /-- If a polynomial of degree 2 is always nonnegative, then its discriminant is nonpositive -/
123 lemma discriminant_le_zero {a b c : α} (h : ∀ x : α, 0 ≤ a*x*x + b*x + c) : discrim a b c ≤ 0 :=
id ┴ ┴ ┴ ┴┴┴┴┴ ┴ ┴┴┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴
typ ┴ ┴ ┴ ┴┴┴┴┴ ┴ ┴┴┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴
doc └─────┘
124 have hc : 0 ≤ c, by { have := h 0, linarith },
id ┴ ┴ ┴
src ┴ └──────┘ └┘ └───────┘
typ ┴ ┴ └──────┘┴└┘ └───────┘
doc └──────┘ └┘ └───────┘
txt └──────┘ └┘ └───────┘
par └──────┘ └┘ └───────┘
pid └───┘└─┘ ┴┴ ┴
st └────────────┘└─────────┘└┘
125 begin
st └─────
126 rw [discrim, pow_two],
id └─────┘ └─────┘
src └──┘└─────┘└┘└─────┘┴
typ └──┘└─────┘└┘└─────┘┴
doc └──┘└─────┘└┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ────────────┘└───────┘└──
127 cases lt_trichotomy a 0 with ha ha,
id └───────────┘ ┴
src └────┘└───────────┘┴ └───────────┘
typ └────┘└───────────┘┴┴└───────────┘
doc └────┘ ┴ └───────────┘
txt └────┘ ┴ └───────────┘
par └────┘ ┴ └───────────┘
pid ┴ ┴ ┴└──────────┘
st ───────────────────────────────────┘└─
128 -- if a < 0
st ──────────────
129 cases classical.em (b = 0) with hb hb,
id └──────────┘ ┴
src └────┘└──────────┘┴ ┴ └────────────┘
typ └────┘└──────────┘┴ ┴┴ └────────────┘
doc └────┘ ┴ ┴ └────────────┘
txt └────┘ ┴ ┴ └────────────┘
par └────┘ ┴ ┴ └────────────┘
pid ┴ ┴ ┴ └─┘└─────────┘
st ──────────────────────────────────────┘└─
130 { rw hb at *,
id └┘
src └─┘ └───┘
typ └─┘└┘└───┘
doc └─┘ └───┘
txt └─┘ └───┘
par └─┘ └───┘
pid ┴ └───┘
st ───┘└────────┘└─
131 rcases exists_lt_mul_self (-c/a) with ⟨x, hx⟩,
id └────────────────┘ ┴┴┴
src └─────┘└────────────────┘┴ ┴ └────────────┘
typ └─────┘└────────────────┘┴ ┴┴┴└────────────┘
doc └─────┘ ┴ └────────────┘
txt └─────┘ ┴ └────────────┘
par └─────┘ ┴ └────────────┘
pid ┴ ┴ └────────────┘
st ────────────────────────────────────────────────┘└─
132 have := mul_lt_mul_of_neg_left hx ha,
id └────────────────────┘ └┘ └┘
src └──────┘└────────────────────┘┴ ┴
typ └──────┘└────────────────────┘┴└┘┴└┘
doc └──────┘ ┴ ┴
txt └──────┘ ┴ ┴
par └──────┘ ┴ ┴
pid └───┘└─┘ ┴ ┴
st ───────────────────────────────────────┘└─
133 rw [mul_div_cancel' _ (ne_of_lt ha), ← mul_assoc] at this,
id └─────────────┘ └──────┘ └┘ └───────┘
src └──┘└─────────────┘└─┘ └──────┘┴ └───┘└───────┘└───────┘
typ └──┘└─────────────┘└─┘ └──────┘┴└┘└───┘└───────┘└───────┘
doc └──┘ └─┘ ┴ └───┘ └───────┘
txt └──┘ └─┘ ┴ └───┘ └───────┘
par └──┘ └─┘ ┴ └───┘ └───────┘
pid └┘ └─┘ ┴ └───┘ ┴└──────┘
st ──────────────────────────────────────┘└───────────┘┴└──────┘└─
134 have h₂ := h x, linarith },
id ┴ ┴
src └─────────┘ ┴ └───────┘
typ └─────────┘┴┴┴ └───────┘
doc └─────────┘ ┴ └───────┘
txt └─────────┘ ┴ └───────┘
par └─────────┘ ┴ └───────┘
pid └─────┘┴└─┘ ┴ ┴
st ─────────────────┘└─────────┘└┘└
135 { cases classical.em (c = 0) with hc' hc',
id └──────────┘ ┴
src └────┘└──────────┘┴ ┴ └──────────────┘
typ └────┘└──────────┘┴ ┴┴ └──────────────┘
doc └────┘ ┴ ┴ └──────────────┘
txt └────┘ ┴ ┴ └──────────────┘
par └────┘ ┴ ┴ └──────────────┘
pid ┴ ┴ ┴ └─┘└───────────┘
st ───┘└─────────────────────────────────────┘└─
136 { rw hc' at *,
id └─┘
src └─┘ └───┘
typ └─┘└─┘└───┘
doc └─┘ └───┘
txt └─┘ └───┘
par └─┘ └───┘
pid ┴ └───┘
st ─────┘└─────────┘└─
137 have : -(a*-b*-b + b*-b + 0) = (1-a)*(b*b), ring,
id ┴┴ ┴
src └─────┘ ┴ ┴ ┴ └──┘ ┴ ┴┴ ┴ ┴ └──┘
typ └─────┘ ┴ ┴ ┴ └──┘ ┴ ┴┴┴┴ ┴┴ └──┘
doc └─────┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └──┘
txt └─────┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └──┘
par └─────┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └──┘
pid └───┘└┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴
st ───────────────────────────────────────────────┘└────┘└─
138 have h := h (-b), rw [← neg_nonpos, this] at h,
id ┴ ┴ └────────┘ └──┘
src └────────┘ ┴ ┴ └────┘└────────┘└┘ └────┘
typ └────────┘┴┴ ┴┴ └────┘└────────┘└┘└──┘└────┘
doc └────────┘ ┴ ┴ └────┘ └┘ └────┘
txt └────────┘ ┴ ┴ └────┘ └┘ └────┘
par └────────┘ ┴ ┴ └────┘ └┘ └────┘
pid └────┘┴└─┘ ┴ ┴ └──┘ └┘ ┴└───┘
st ─────────────────────┘└────────────────┘└────┘┴└───┘└─
139 have : b * b ≤ 0, from nonpos_of_mul_nonpos_left h (by linarith),
id ┴ ┴ └───────────────────────┘ ┴
src └─────┘ ┴ ┴ ┴┴└┘ └───┘└───────────────────────┘┴ ┴ ┴└──────┘┴
typ └─────┘ ┴ ┴┴┴┴└┘ └───┘└───────────────────────┘┴┴┴ ┴└──────┘┴
doc └─────┘ ┴ ┴ ┴ └┘ └───┘ ┴ ┴ ┴└──────┘┴
txt └─────┘ ┴ ┴ ┴ └┘ └───┘ ┴ ┴ ┴└──────┘┴
par └─────┘ ┴ ┴ ┴ └┘ └───┘ ┴ ┴ ┴└──────┘┴
pid └───┘└┘ ┴ ┴ ┴ ┴┴ └───┘ ┴ ┴ └────────┘
st ─────────────────────┘└────────────────────────────────────┘└───────┘┴└─
140 linarith },
src └───────┘
typ └───────┘
doc └───────┘
txt └───────┘
par └───────┘
pid ┴
st ──────────────┘└┘└
141 { have h := h (-c/b),
id ┴ ┴ ┴
src └────────┘ ┴ ┴
typ └────────┘┴┴ ┴ ┴┴
doc └────────┘ ┴ ┴
txt └────────┘ ┴ ┴
par └────────┘ ┴ ┴
pid └────┘┴└─┘ ┴ ┴
st ───────────────────────┘└─
142 have : a*(-c/b)*(-c/b) + b*(-c/b) + c = a*((c/b)*(c/b)),
id ┴ ┴ ┴
src └─────┘ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ └┘
typ └─────┘ ┴ └┘ ┴ └┘ ┴ ┴ ┴┴ ┴ ┴ ┴└┘
doc └─────┘ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ └┘
txt └─────┘ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ └┘
par └─────┘ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ └┘
pid └───┘└┘ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ └┘
st ────────────────────────────────────────────────────────────┘└─
143 rw mul_div_cancel' _ hb, ring,
id └─────────────┘ └┘
src └─┘└─────────────┘└─┘ └──┘
typ └─┘└─────────────┘└─┘└┘ └──┘
doc └─┘ └─┘ └──┘
txt └─┘ └─┘ └──┘
par └─┘ └─┘ └──┘
pid ┴ └─┘
st ──────────────────────────────┘└────┘└─
144 rw this at h,
id └──┘
src └─┘ └───┘
typ └─┘└──┘└───┘
doc └─┘ └───┘
txt └─┘ └───┘
par └─┘ └───┘
pid ┴ └───┘
st ─────────────────┘└─
145 have : 0 ≤ a := nonneg_of_mul_nonneg_right h (mul_self_pos $ div_ne_zero hc' hb),
id ┴ └────────────────────────┘ ┴ └──────────┘ └─────────┘ └─┘ └┘
src └───────┘ ┴ └──┘└────────────────────────┘┴ ┴ └──────────┘┴ ┴└─────────┘┴ ┴ ┴
typ └───────┘ ┴┴└──┘└────────────────────────┘┴┴┴ └──────────┘┴ ┴└─────────┘┴└─┘┴└┘┴
doc └───────┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
txt └───────┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par └───────┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid └───┘└──┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ─────────────────────────────────────────────────────────────────────────────────────┘└─
146 linarith [ha] } },
id └┘
src └────────┘ └┘
typ └────────┘└┘└┘
doc └────────┘ └┘
txt └────────┘ └┘
par └────────┘ └┘
pid ┴┴ ┴┴
st ───────────────────┘└──┘└
147 cases ha with ha ha,
id └┘
src └────┘ └─────────┘
typ └────┘└┘└─────────┘
doc └────┘ └─────────┘
txt └────┘ └─────────┘
par └────┘ └─────────┘
pid ┴ └─────────┘
st ────────────────────┘└─
148 -- if a = 0
st ──────────────
149 cases classical.em (b = 0) with hb hb,
id └──────────┘ ┴
src └────┘└──────────┘┴ ┴ └────────────┘
typ └────┘└──────────┘┴ ┴┴ └────────────┘
doc └────┘ ┴ ┴ └────────────┘
txt └────┘ ┴ ┴ └────────────┘
par └────┘ ┴ ┴ └────────────┘
pid ┴ ┴ ┴ └─┘└─────────┘
st ──────────────────────────────────────┘└─
150 { rw [ha, hb], linarith },
id └┘ └┘
src └──┘ └┘ ┴ └───────┘
typ └──┘└┘└┘└┘┴ └───────┘
doc └──┘ └┘ ┴ └───────┘
txt └──┘ └┘ ┴ └───────┘
par └──┘ └┘ ┴ └───────┘
pid └┘ └┘ ┴ ┴
st ─────┘└────┘└──┘┴└─────────┘└┘└
151 { have := h ((-c-1)/b), rw [ha, mul_div_cancel' _ hb] at this, linarith },
id ┴ ┴ ┴ └┘ └─────────────┘ └┘
src └──────┘ ┴ └┘ ┴ └──┘ └┘└─────────────┘└─┘ └───────┘ └───────┘
typ └──────┘┴┴ ┴ └┘ ┴┴ └──┘└┘└┘└─────────────┘└─┘└┘└───────┘ └───────┘
doc └──────┘ ┴ └┘ ┴ └──┘ └┘ └─┘ └───────┘ └───────┘
txt └──────┘ ┴ └┘ ┴ └──┘ └┘ └─┘ └───────┘ └───────┘
par └──────┘ ┴ └┘ ┴ └──┘ └┘ └─┘ └───────┘ └───────┘
pid └───┘└─┘ ┴ └┘ ┴ └┘ └┘ └─┘ ┴└──────┘ ┴
st ─────┘└──────────────────┘└──────┘└────────────────────┘┴└──────┘└─────────┘└┘└
152 -- if a > 0
st ──────────────
153 have := calc
src └──────┘ └
typ └──────┘ └
doc └──────┘ └
txt └──────┘ └
par └──────┘ └
pid └───┘└─┘ └
st ───────────────
154 4*a* (a*(-(b/a)*(1/2))*(-(b/a)*(1/2)) + b*(-(b/a)*(1/2)) + c)
src ────┘ ┴ ┴ ┴ └─┘ ┴ ┴ └──┘ ┴ ┴ ┴ └──┘ ┴ └─
typ ────┘ ┴ ┴ ┴ └─┘ ┴ ┴ └──┘ ┴ ┴ ┴ └──┘ ┴ └─
doc ────┘ ┴ ┴ ┴ └─┘ ┴ ┴ └──┘ ┴ ┴ ┴ └──┘ ┴ └─
txt ────┘ ┴ ┴ ┴ └─┘ ┴ ┴ └──┘ ┴ ┴ ┴ └──┘ ┴ └─
par ────┘ ┴ ┴ ┴ └─┘ ┴ ┴ └──┘ ┴ ┴ ┴ └──┘ ┴ └─
pid ────┘ ┴ ┴ ┴ └─┘ ┴ ┴ └──┘ ┴ ┴ ┴ └──┘ ┴ └─
st ──────────────────────────────────────────────────────────────────
155 = (a*(b/a)) * (a*(b/a)) - 2*(a*(b/a))*b + 4*a*c : by ring
src ─────┘ ┴ └─┘ ┴ └─┘ └┘ └┘ ┴ └┘ └─┘ ┴└────
typ ─────┘ ┴ └─┘ ┴ └─┘ └┘ └┘ ┴ └┘ └─┘ ┴└────
doc ─────┘ ┴ └─┘ ┴ └─┘ └┘ └┘ ┴ └┘ └─┘ ┴└────
txt ─────┘ ┴ └─┘ ┴ └─┘ └┘ └┘ ┴ └┘ └─┘ ┴└────
par ─────┘ ┴ └─┘ ┴ └─┘ └┘ └┘ ┴ └┘ └─┘ ┴└────
pid ─────┘ ┴ └─┘ ┴ └─┘ └┘ └┘ ┴ └┘ └─┘ └─────
st ─────────────────────────────────────────────────────────┘└─────
156 ... = -(b*b - 4*a*c) : by { simp only [mul_div_cancel' b (ne_of_gt ha)], ring },
id ┴ ┴ ┴ └─────────────┘ ┴ └──────┘ └┘
src ───┘└──┘ ┴ ┴ └┘ └──┘ └─┘└─────────┘└─────────────┘┴ ┴ └──────┘┴ └┘└┘└───┘┴
typ ───┘└──┘ ┴ ┴┴ └┘ ┴ ┴└──┘ └─┘└─────────┘└─────────────┘┴┴┴ └──────┘┴└┘└┘└┘└───┘┴
doc ───┘└──┘ ┴ ┴ └┘ └──┘ └─┘└─────────┘ ┴ ┴ ┴ └┘└┘└───┘┴
txt ───┘└──┘ ┴ ┴ └┘ └──┘ └─┘└─────────┘ ┴ ┴ ┴ └┘└┘└───┘┴
par ───┘└──┘ ┴ ┴ └┘ └──┘ └─┘└─────────┘ ┴ ┴ ┴ └┘└┘└───┘┴
pid ───────┘ ┴ ┴ └┘ └──┘ └────────────┘ ┴ ┴ ┴ └────────┘
st ───┘└───────────────────────┘└────────────────────────────────────────────┘└─────┘└┘└
157 have ha' : 0 ≤ 4*a, linarith,
id ┴
src └───────────┘ └┘ └──────┘
typ └───────────┘ └┘ ┴ └──────┘
doc └───────────┘ └┘ └──────┘
txt └───────────┘ └┘ └──────┘
par └───────────┘ └┘ └──────┘
pid └──────┘└───┘ └┘
st ───────────────────┘└────────┘└─
158 have h := (mul_nonneg ha' (h (-(b/a) * (1/2)))),
id └────────┘ └─┘ ┴ ┴ ┴
src └────────┘ └────────┘┴ ┴ ┴ └┘ ┴ ┴ └───┘
typ └────────┘ └────────┘┴└─┘┴ ┴┴ ┴ ┴└┘ ┴ ┴ └───┘
doc └────────┘ ┴ ┴ ┴ └┘ ┴ ┴ └───┘
txt └────────┘ ┴ ┴ ┴ └┘ ┴ ┴ └───┘
par └────────┘ ┴ ┴ ┴ └┘ ┴ ┴ └───┘
pid └────┘┴└─┘ ┴ ┴ ┴ └┘ ┴ ┴ └───┘
st ────────────────────────────────────────────────┘└─
159 rw this at h, rwa ← neg_nonneg
id └──┘ └────────┘
src └─┘ └───┘ └────┘└────────┘┴
typ └─┘└──┘└───┘ └────┘└────────┘┴
doc └─┘ └───┘ └────┘ ┴
txt └─┘ └───┘ └────┘ ┴
par └─┘ └───┘ └────┘ ┴
pid ┴ └───┘ └─┘ ┴
st ─────────────┘└─────────────────┘
160 end
st └─┘
161
162 /--
163 If a polynomial of degree 2 is always positive, then its discriminant is negative,
164 at least when the coefficient of the quadratic term is nonzero.
165 -/
166 lemma discriminant_lt_zero {a b c : α} (ha : a ≠ 0) (h : ∀ x : α, 0 < a*x*x + b*x + c) :
id ┴ ┴ ┴ ┴ ┴ ┴┴┴┴┴ ┴ ┴┴┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴┴┴┴┴ ┴ ┴┴┴ ┴ ┴
167 discrim a b c < 0 :=
id └─────┘ ┴ ┴ ┴ ┴
src └─────┘ ┴
typ └─────┘ ┴ ┴ ┴ ┴
doc └─────┘
168 begin
st └─────
169 have : ∀ x : α, 0 ≤ a*x*x + b*x + c := assume x, le_of_lt (h x),
id ┴ ┴ ┴┴ ┴ ┴ ┴ └──────┘ ┴
src └─────┘ └───┘ └──┘┴┴ ┴ ┴┴┴ ┴ ┴ └──┘ └──┘└──────┘┴ ┴ ┴
typ └─────┘ └───┘┴ └──┘┴┴┴┴ ┴┴┴┴ ┴ ┴┴└──┘ └──┘└──────┘┴ ┴┴ ┴
doc └─────┘ └───┘ └──┘ ┴ ┴ ┴ ┴ ┴ └──┘ └──┘ ┴ ┴ ┴
txt └─────┘ └───┘ └──┘ ┴ ┴ ┴ ┴ ┴ └──┘ └──┘ ┴ ┴ ┴
par └─────┘ └───┘ └──┘ ┴ ┴ ┴ ┴ ┴ └──┘ └──┘ ┴ ┴ ┴
pid └───┘└┘ └───┘ └──┘ ┴ ┴ ┴ ┴ ┴ └──┘ └──┘ ┴ ┴ ┴
st ─────────────────────────────────────────────────────────────────┘└─
170 refine lt_of_le_of_ne (discriminant_le_zero this) _,
id └────────────┘ └──────────────────┘ └──┘
src └─────┘└────────────┘┴ └──────────────────┘┴ └─┘
typ └─────┘└────────────┘┴ └──────────────────┘┴└──┘└─┘
doc └─────┘ ┴ └──────────────────┘┴ └─┘
txt └─────┘ ┴ ┴ └─┘
par └─────┘ ┴ ┴ └─┘
pid ┴ ┴ ┴ └─┘
st ────────────────────────────────────────────────────┘└─
171 assume h',
src └───────┘
typ └───────┘
doc └───────┘
txt └───────┘
par └───────┘
pid └───────┘
st ──────────┘└─
172 have := h (-b / (2 * a)),
id ┴ ┴┴ ┴ ┴
src └──────┘ ┴ ┴ ┴┴┴ └┘ ┴ └┘
typ └──────┘┴┴ ┴┴┴┴┴ └┘ ┴┴└┘
doc └──────┘ ┴ ┴ ┴ └┘ ┴ └┘
txt └──────┘ ┴ ┴ ┴ └┘ ┴ └┘
par └──────┘ ┴ ┴ ┴ └┘ ┴ └┘
pid └───┘└─┘ ┴ ┴ ┴ └┘ ┴ └┘
st ─────────────────────────┘└─
173 have : a * (-b / (2 * a)) * (-b / (2 * a)) + b * (-b / (2 * a)) + c = 0,
id ┴ ┴ ┴ ┴
src └─────┘ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ ┴┴└┘
typ └─────┘ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ ┴┴ ┴ └┘ ┴┴└─┘ ┴┴┴┴└┘
doc └─────┘ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ ┴ └┘
txt └─────┘ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ ┴ └┘
par └─────┘ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ ┴ └┘
pid └───┘└┘ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ ┴ ┴┴
st ────────────────────────────────────────────────────────────────────────┘└─
174 rw [quadratic_eq_zero_iff_of_discrim_eq_zero ha h' (-b / (2 * a))],
id └──────────────────────────────────────┘ └┘ └┘ ┴ ┴
src └──┘└──────────────────────────────────────┘┴ ┴ ┴ ┴ ┴ └┘ ┴ └─┘
typ └──┘└──────────────────────────────────────┘┴└┘┴└┘┴ ┴┴ ┴ └┘ ┴┴└─┘
doc └──┘└──────────────────────────────────────┘┴ ┴ ┴ ┴ ┴ └┘ ┴ └─┘
txt └──┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └─┘
par └──┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └─┘
pid └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └─┘
st ────────────────────────────────────────────────────────────────────┘└──
175 linarith
src └───────┘
typ └───────┘
doc └───────┘
txt └───────┘
par └───────┘
pid ┴
st ──────────┘
176 end
st └─┘